package systemfnomabss

/**
 * Slightly adapted from parser for untyped lambda calculus by Miles Sabin 
 */
    
import scala.util.parsing.input.Reader
import scala.util.parsing.input.StreamReader
import java.io.StringReader
import scala.util.parsing.combinatorold.lexical.StdLexical
import scala.util.parsing.combinatorold.syntactical.StdTokenParsers
import scala.util.parsing.combinatorold.ImplicitConversions


trait systemfLambdaToTextualParser extends StdTokenParsers  with ImplicitConversions with TextualSyntax
{
  
   def parseString(str: String) : Option[RTerm]= {
     val in = StreamReader(new StringReader(str))
     parse(in) match
     {
     case Success(term, _) =>
     {
       Some(term)
     }
     case Failure(msg, remainder) => println("Failure: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString) ;None
     case Error(msg, remainder)   => println("Error: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString) ; None
   }
   }

  //type RawTerm = RTerm
  type Tokens = StdLexical
  val lexical = new StdLexical
  lexical.reserved ++= List("unit", "let", "in", "if", "then", "else","bool","int","true", "false","from","fld", "forall", "forsome", "import", "into","as")
  lexical.delimiters ++= List("=>", ",",":", ".", ";", "_", "==", "(", ")", "{","}", "]", "[","=", "\\", "\\[]", "+", "-", "{*", "/")

  
  
  
  def parse(r: Reader[char]) : ParseResult[RawTerm] =
    phrase(expr)(new lexical.Scanner(r))
  

    
  def expr : Parser[RawTerm] = expr3
  
  //def expr2 : Parser[RawTerm] =  chainl1(expr3, typeinbrackets, success(TyApplic(_: RawTerm, _: LType)))
 
  def expr3 : Parser[RawTerm] =  chainl1(expr4, success(RApp(_: RawTerm, _: RawTerm)))
  
  def expr4 : Parser[RawTerm] =  chainl1(expr5, ident, "." ^^ {(a: RawTerm, b: String) => RRecProj(a,b)})
   
  def expr5 : Parser[RawTerm] =
  ( "\\"   ~ lambdas  
  | "\\[]" ~ typelambdas

  | "if" ~ expr ~ "then" ~ expr ~ "else" ~ expr ^^ flatten3(RIf)
  | "let" ~ termvarname ~ "=" ~ expr ~ "in" ~ expr ^^ flatten3(RLet)
  
  | "{" ~ repsep(recordel,",") ~ "}" ^^ RRecord
  | "from" ~expr~ "fld" ~ident ^^ flatten2(RRecProj)

  | pack
 | "import" ~ expr ~ "into" ~ "{" ~ typevarname ~","~ termvarname~ "}" ~ "in" ~ expr  ^^ flatten4(RUnpack)

  | tyapp
  | simpleexpr
  
  )
  

 
  def termvarname : Parser[RVarName] = "_" ^^ RVarName("_") | ident ^^ RVarName 
  def typevarname : Parser[RTyVarName] = "_" ^^ RTyVarName("_") | ident ^^ RTyVarName 

  def lambdas : Parser[RawTerm] = 
    termvarname ~ ":" ~ ltype ~ ("." ~ expr4 | lambdas ) ^^ flatten3(RLam)
  def typelambdas : Parser[RawTerm] =
    typevarname               ~ ("." ~ expr4 ) ^^ flatten2(RTLam)
      
    
  def recordel = ident ~ "="~expr ^^ flatten2(Tuple2[String,RawTerm])
  def tyrecordel = ident ~ ":"~ltype ^^ flatten2(Tuple2[String, RType])
  
    
  def tyapp : Parser[RawTerm] = 
    simpleexpr ~ typeinbrackets   ^^ flatten2(RTApp)
    
  def pack : Parser[RawTerm] = 
    "{*" ~ ltype ~ "," ~ expr ~"}" ~ "as" ~  ltype ^^ flatten3(RPack)
 
   
  def typeinbrackets: Parser[RType] = "[" ~ ltype ~ "]" 
    
  def simpleexpr : Parser[RawTerm] =
    ( numericLit ^^ (_.toInt) ^^ RLit
    | termvarname 
    | "true" ^^ RTru()
    | "false" ^^ RFls()
    | ( "unit" ^^ RUnit() )
    | "(" ~expr~ ")"
    
    )
  

  
    
  def ltype : Parser[RType]  =
    ( "bool" ^^ RTyBool()
    | "int" ^^ RTyInt()
    | "unit" ^^ RTyUnit()
    | typevarname 
    | "{" ~ repsep(tyrecordel,",") ~ "}" ^^ RTyRecord
    | "(" ~ ltype ~ "=>" ~ ltype ~ ")" ^^ flatten2(RTyArr)
    | "forall" ~ typevarname ~ "." ~ ltype ^^ flatten2(RTyUniv)
    | ("{" ~ "forsome" ~ typevarname ~"," ~ ltype ~ "}" ^^ flatten2(RTyExist) )
    )
  

  

}